hsk

% ------------------------   SYNTAX  ------------------------

m(M) :- M = true
      ; M = false
      ; M = if(M1,M2,M3)     , m(M1),m(M2),m(M3)
      ; M = zero
      ; M = succ(M1)         , m(M1)
      ; M = pred(M1)         , m(M1)
      ; M = iszero(M1)       , m(M1)
      .

hsk

% Implementation on Prolog of The Design and Implementation of Typed Scheme 
:- op(1200,xfx,[::=]),op(600,xfx,[∈,<:,:>]).
:- op(990,xfx,[⊢]),op(990,fy,[⊢]).
:- op(250,yf,[*]).
:- op(920, xfx, ['→', '↠']).
:- op(600,yfx,[$]).
G∈(G|_). G∈(_|G2):-G∈G2. G∈G :- G\=(_|_).
bnf(S/[S2],AEs) :- compound_name_arguments(AEs,A,Es),bnf(S,A),bnf(S2,Es).
bnf(G,E):-G=..[O|Gs],E=..[O|Es],maplist(bnf,Gs,Es),!.
bnf(G,E):-(G::=Gs),!,G1∈Gs,bnf(G1,E),!.

hsk

#lang racket
(require redex)
(provide λ λV ev)

(define-language λ
  (e ::= (e e) x (λ (x τ) e) (if0 e e e) (e + e) n)
  (n ::= number)
  (τ ::= (τ -> τ) num)
  (x ::= variable-not-otherwise-mentioned))

hsk

use nom::bytes::complete::tag;
use nom::character::complete::multispace0;
use nom::combinator::map;
use nom::error::VerboseError;
use nom::sequence::tuple;
use nom::IResult;
struct Ctx {
    a: i32
}
impl Ctx {

hsk

use nom;
use nom::{
    bytes::complete::{tag, take_until, take_while1},
    branch::alt,
    character::complete::{char, multispace0},
    combinator::{map, cut},
    error::VerboseError,
    multi::{many1,separated_list0},
    sequence::{preceded, terminated, tuple, separated_pair},
    IResult,

hsk

/*
このプログラムはswi-prologで実行することができます。
swiproogのインストールは以下のようにしてインストールできます:
$ brew install swi-prolog
$ apt install swi-prolog
このプログラムを実行するには以下のようにコマンドラインから実行します:
$ swipl math.pl

現代数学は一階述語論理を道具としてペアノ数などを定義していくことで構築されています。
http://www.f.waseda.jp/moriya/PUBLIC_HTML/social/natural_numbers.pdf

hsk

import scala.collection.mutable.{Set => MutSet}
object simplesub1 extends App {
  sealed trait Term
  final case class Lit(value: Int) extends Term                         // as in: 27
  final case class Var(name: String) extends Term                       // as in: x
  final case class Lam(name: String, rhs: Term) extends Term            // as in: λx . t
  final case class App(lhs: Term, rhs: Term) extends Term               // as in: s t
  final case class Rcd(fields: List[(String, Term)]) extends Term       // as in: { a : 0; b : true; ... }
  final case class Sel(receiver: Term, fieldName: String) extends Term  // as in: t .a

hsk

/*
https://letexpr.hatenablog.com/entry/2018/11/15/222959
%ast
term ::= string
       | bool(qual,bool)
       | if(term, term , term)
       | (qual, term, term)
       | let((string, string)=term, term)
       | λ(qual, string: ltype, term)
       | app(term, term).

hsk

% https://qiita.com/fukkun/items/05160e8dae0e15ae201e
reset:- nb_setval(cnt,0),retractall(tmp(_,_)).
genid(C1):- nb_getval(cnt,C),C1 is C+1,nb_setval(cnt,C1).
gentmp(T):- genid(C),atomic_list_concat([t,C],T).
gentmp(E,T):- tmp(E,T).
gentmp(E,T):- gentmp(T),assert(tmp(E,T)).
tran([N:(X=A+B)|C],[N:(T=A+B),NA:(X=T)|C_]) :- gentmp(A+B,T),atom_concat(N,*,NA),tran(C,C_).
tran([N:(X=A-B)|C],[N:(T=A-B),NA:(X=T)|C_]) :- gentmp(A-B,T),atom_concat(N,*,NA),tran(C,C_).
tran([N:I|C],[N:I|C_]):- tran(C,C_).
tran([],[]).

hsk

ops(+,1).
ops(*,2).
parse(O,S,[],R):-!,parse3(O,S,R).
parse(O,S,['('|C],R):-!,parse(O,['('|S],C,R).
parse(O,S,[')'|C],R):-!,parse1(O,S,C,R).
parse(O,S,[A|C],R):-atom_number(A,I),!,parse([I|O],S,C,R).
parse(O,S,[V|C],R):-ops(V,P),!,parse2(P,O,S,[V|C],R).
parse(_,_,_,_):-throw('InvalidToken').
parse1(_,[],_,_):-throw('ParenthesisMismatch').
parse1(O,['('|S],C,R):-parse(O,S,C,R).